./fix-syntax ./prism -javamaxmem 11g -cuddmaxmem 4g -ii -e 5e-2 -heuristic speed -ddextraactionvars 100 -maxiters 1000000 resource-gathering.pm resource-gathering.prctl --property expsteps -const B=1300,GOLD_TO_COLLECT=100,GEM_TO_COLLECT=100
PRISM
=====
Version: 4.5.dev
Date: Sat Mar 14 23:42:39 UTC 2020
Hostname: e72bdd194fc5
Memory limits: cudd=4g, java(heap)=11g
Command line: prism -javamaxmem 11g -cuddmaxmem 4g -ii -e 5e-2 -heuristic speed -ddextraactionvars 100 -maxiters 1000000 resource-gathering.pm_fixed resource-gathering.prctl_fixed --property expsteps -const 'B=1300,GOLD_TO_COLLECT=100,GEM_TO_COLLECT=100'
Parsing model file "resource-gathering.pm_fixed"...
Type: MDP
Modules: robot goldcounter gemcounter
Variables: gold gem attacked x y required_gold required_gem
Parsing properties file "resource-gathering.prctl_fixed"...
3 properties:
(1) "expgold": R{"rew_gold"}max=? [ C<=B ]
(2) "expsteps": R{"time_reward"}min=? [ F "success" ]
(3) "prgoldgem": Pmax=? [ F<=B "success" ]
---------------------------------------------------------------------
Model checking: "expsteps": R{"time_reward"}min=? [ F "success" ]
Model constants: GOLD_TO_COLLECT=100,GEM_TO_COLLECT=100,B=1300
Warning: Switching to sparse engine and (backwards) Gauss Seidel (default for heuristic=speed).
Warning: Switching to explicit engine to allow interval iteration on Rmin operator.
Building model...
Model constants: GOLD_TO_COLLECT=100,GEM_TO_COLLECT=100,B=1300
Computing reachable states... 190863 392773 576522 772596 957649 958894 states
Reachable states exploration and model construction done in 15.031 secs.
Sorting reachable states list...
Time for model construction: 17.497 seconds.
Type: MDP
States: 958894 (1 initial)
Transitions: 3325526
Choices: 3080702
Max/avg: 4/3.21
Building reward structure...
Starting expected reachability (min)...
Starting Prob1 (max)...
Prob1 (max) took 1203 iterations and 49.933 seconds.
target=94, inf=0, rest=958800
For Rmin, checking for zero-reward ECs...
Time for checking for zero-reward ECs: 0.232 seconds, no zero-reward ECs found, proceeding normally.
Computing upper bound(s) for Rmin using the Dijkstra Sweep for Monotone Pessimistic Initialization algorithm...
Calculating incoming choices relation for Markov decision process... done (0.305 seconds)
Time for computing upper bound(s) for Rmin using the DSI-MP algorithm: 3.08 seconds.
Upper bound for min expectation (Dijkstra Sweep MPI): 1800.0
Starting Prob1 (min)...
Prob1 (min) took 2 iterations and 0.138 seconds.
Error: Interval iteration for Rmin and non-contracting MDP currently not supported.
Overall running time: 71.757 seconds.
---------------------------------------------------------------------
Note: There were 2 warnings during computation.